the_es:ES, e:E. val(e)  valtype(e) 

latex

Definitions	t  T, Id, x:A. B(x), loc(e), f(a), tag(k), lnk(k), act(k), islocal(k), isrcv(k), kindcase(k; a.f(a); l,t.g(l;t) ), x:AB(x), left+right, Knd, x:AB(x), P  Q, s = t, Type, if b t else f fi, P & Q, es_info(es), kind(e), act(e), loc(e), es-V(es), tag(e), lnk(e), es-M(es), es_val(es), acttype(e), rcvtype(e), isrcv(e), val(e), valtype(e), E, ES, kind(e)
Lemmas	event system wf, kind wf, Knd wf, subtype rel self, loc wf, Id wf